M1, M2:MsgA.
M1  M2  (k:Knd, l:IdLnk, tg:Id. M2.sframe(k sends <l,tg>)  M1.sframe(k sends <l,tg>)) 

latex

Definitions	x:A. B(x), P  Q, M.sframe(k sends <l,tg>), t.1, t.2, z != f(x)  P(a;z), t  T, , T, True, x. t(x), MsgA, M1  M2, Valtype(da;k), A c B, P & Q, f  g, x(s)
Lemmas	assert wf, squash wf, true wf, bool wf, deq-member wf, deq wf, Knd wf, Kind-deq wf, fpf-dom wf, IdLnk wf, Id wf, product-deq wf, idlnk-deq wf, id-deq wf, fpf-trivial-subtype-top, ma-sframe wf, ma-sub wf, msga wf